p:FinProbSpace, f:(), X, Y:(n:RandomVariable(p;f(n))).
rv-iid(p;n.f(n);n.X(n))
 rv-iid(p;n.f(n);n.Y(n))
 (n:, i:{0..(n+1)}. rv-disjoint(p;f(n);Y(i);X(n)) & rv-disjoint(p;f(n);X(i);Y(n)))
 rv-iid(p;n.f(n);n.X(n) + Y(n)) 

latex

Definitions

x:A  B(x), rv-identically-distributed(p;n.f(n);i.X(i)), rv-disjoint(p;n;X;Y), P & Q, x:AB(x), rv-iid(p;n.f(n);i.X(i)), t  T, {x:A| B(x)} , i  j < k, f(a), FinProbSpace, P  Q, False, A, , Type, <a, b>, True, T, {T}, SQType(T), s ~ t, Void, left + right, P  Q, Dec(P), x:A.B(x), Top, , type List, S  T, , A  B, , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), x,y. t(x;y), x,y:A//B(x;y), ||as||, x. t(x), x(s), a < b, , s = t, A  B, RandomVariable(p;n), #$n, n+m, {i..j}, x:A. B(x), , (x.F(x)) o X, X * Y, E(n;F), r * s, P  Q, P  Q, r + s, X + Y, , (x  l), r  s, xL. P(x), l[i], a  j < b. E(j), A c B

Lemmas

rv-disjoint-rv-add2, rv-disjoint-rv-add, qsum wf, select wf, l all wf2, qle wf, l member wf, length wf1, expectation-rv-add, expectation-rv-add-squared, expectation-rv-add-cubed, rv-compose wf, rv-add wf, expectation-rv-add-fourth, int inc rationals, expectation wf, rv-disjoint-rv-mul2, qadd wf, expectation-rv-disjoint, nat properties, rv-mul wf, rv-disjoint-rv-mul, int-rational, qmul wf, rv-iid wf, finite-prob-space wf, subtype rel function, int seg properties, subtype rel weakening, ext-eq weakening, length wf nat, quotient wf, bool wf, qeq wf2, btrue wf, b-union wf, int nzero wf, top wf, rationals wf, decidable int equal, squash wf, true wf, nat wf, int seg wf, rv-disjoint wf, random-variable wf, le wf